\begin{thebibliography}{99}

\bibitem{Nuprl} % OK
S.F.\ Allen, R.L.\ Constable, D.J.\ Howe and W.E. Aitken,
`The Semantics of Reflected Proof',
{\it Proceedings of the 5th IEEE Symposium on Logic in Computer Science\/},
pp.\ 95--105, 1990.

\bibitem{BoyerMoore} % OK
R.S.\ Boyer and J\ S.\ Moore, `Metafunctions: Proving Them Correct and
Using Them Efficiently as New Proof Procedures', in: {\it The
Correctness Problem in Computer Science}, edited by
R.S.\ Boyer and J\ S.\ Moore, Academic Press, New York, 1981.

\bibitem{Camilleri-et-al} % OK
A.J.\ Camilleri, T.F.\ Melham and M.J.C. Gordon,
`Hardware Verification using Higher-Order Logic',
in: {\it From HDL Descriptions to Guaranteed Correct \mbox{Circuit}
Designs: Proceedings of the IFIP WG 10.2 Working Conference, Grenoble,
September 1986}, edited by D.\ Borrione (North-Holland, 1987), pp.\ 43--67.

\bibitem{DPLL-paper}
M.\ Davis, G.\ Logemann and D.\ Loveland, `A machine program for
theorem proving', {\it Communications of the ACM}, Vol.\ 5 (1962),
pp.\ 394--397.

\bibitem{Why-HOL-paper} % OK
M.\ Gordon,
`Why higher-order Logic
is a good formalism for specifying and verifying hardware',
in: {\it Formal Aspects of VLSI Design: Proceedings of the 1985 Edinburgh
      Workshop on VLSI\/}, edited by G.\ Milne and
P.A.\ Subrahmanyam (North-Holland, 1986), pp.\ 153--177.

\bibitem{knuth73} % OK
Donald.\ E. Knuth.
{\em The Art of Computer Programming}. Volume 1/Fundamental
  Algorithms. Addison-Wesley, second edition, 1973.

\bibitem{maclane67}
Saunders\ Mac Lane and Garrett Birkhoff. {\em Algebra}.
Collier-MacMillan Limited, London, 1967.

\bibitem{Milner-types}  % OK
R. Milner,
`A Theory of Type Polymorphism in Programming',
{\it Journal of Computer and System Sciences}, Vol.\ 17 (1978),
pp.\ 348--375.

\bibitem{mostow63}   % OK
George\ D. Mostow, Joseph\ H. Sampson, and Jean-Pierre Meyer.
{\em Fundamental Structures of Algebra}. McGraw-Hill Book Company, 1963.

\bibitem{lcp-rewrite} % OK
L.\ Paulson,
`A Higher-Order Implementation of Rewriting',
{\it Science of Computer Programming}, Vol.\ 3, (1983), pp.\ 119--149.

\bibitem{new-LCF-man} % OK
 L.\ Paulson,
{\it Logic and Computation: Interactive Proof with Cambridge LCF},
Cambridge Tracts in Theoretical Computer Science 2
(Cambridge University Press, 1987).

\bibitem{FOL} % OK
R.E.\ Weyhrauch, `Prolegomena to a theory of mechanized formal reasoning',
{\it Artificial Intelligence\/} {\bf 3(1)}, 1980, pp.\ 133--170.

\bibitem{Principia} % OK
A.N.\ Whitehead and B.\ Russell,
{\it Principia Mathematica},
3 volumes (Cambridge University Press, 1910--3).

\end{thebibliography}


%%% Local Variables:
%%% mode: latex
%%% TeX-master: "tutorial"
%%% End:
